\begin{tabbing}
$\forall$${\it poss}$:(ES\{i\}$\rightarrow\mathbb{P}$\{i'\}), $R$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$possible{-}event\{i:l\}(${\it poss}$)$\rightarrow\mathbb{P}$\{i'\}).
\\[0ex]Trans(possible{-}event\=\{i:l\}\+
\\[0ex](${\it poss}$);$1$,$2$.$R$($1$,$2$))
\-\\[0ex]$\Rightarrow$ ($\forall$$e_{1}$, $e_{2}$:possible{-}event\{i:l\}(${\it poss}$). poss{-}le\{i:l\}($e_{1}$; $e_{2}$) $\Rightarrow$ ($R$($e_{1}$,$e_{2}$)))
\\[0ex]$\Rightarrow$ \=($\forall$$P$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow\mathbb{P}$\{i'\}), $e_{1}$, $e_{2}$:possible{-}event\{i:l\}(${\it poss}$).\+
\\[0ex]poss{-}le\{i:l\}($e_{1}$; $e_{2}$) $\Rightarrow$ es{-}knows\{i:l\}(${\it poss}$; $R$; $P$; $e_{1}$) $\Rightarrow$ es{-}knows\{i:l\}(${\it poss}$; $R$; $P$; $e_{2}$))
\-
\end{tabbing}